\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} , $p$, $q$, ${\it p'}$,\+
\\[0ex]${\it q'}$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow$\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\-\\[0ex]($\forall$$a$, $b$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} .
\\[0ex]($a$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($b$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($p$($a$,$b$) $\Leftarrow\!\Rightarrow$ ${\it p'}$($a$,$b$)))
\\[0ex]$\Rightarrow$ \=($\forall$$a$, $b$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} .\+
\\[0ex]($a$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($b$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($q$($a$,$b$) $\Leftarrow\!\Rightarrow$ ${\it q'}$($a$,$b$)))
\-\\[0ex]$\Rightarrow$ ([$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].$p$($a$,$b$))$\ast$[$a$,$b$].$q$($a$,$b$) $\Leftarrow\!\Rightarrow$ [$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].${\it p'}$($a$,$b$))$\ast$[$a$,$b$].${\it q'}$($a$,$b$))
\end{tabbing}